Inference at * 2 1 1 
Iof proof for Lemma p-fun-exp-add-sq:



1. A : Type
2. f : A(A + Top)
3. x : A
4. m : 
5. 0 < m
6. n:. (can-apply(f^m - 1;x))  ((f^n+(m - 1)(x)) ~ (f^n(do-apply(f^m - 1;x))))
7. n : 
8. can-apply(f^m;x)
9. n = 0
  (f^m(x)) ~ (f^0(do-apply(f^m;x))) 

latex

 by (((Unfolds ``p-fun-exp`` ( 0)) 
CollapseTHEN (Reduce 0)) 
CollapseTHEN ((Fold `p-fun-exp` 0
C) 
CollapseTHEN (RepUR ``p-id`` ( 0)))) 
CollapseTHEN ((RWO "inl-do-apply" 0) 

CoCollapseTHEN (Auto)) 

latex

C.

Definitions	p-id(), f^n, , {x:A| B(x)} , A, False, P  Q, x:AB(x), Void, a < b, A  B, x:A. B(x), t  T
Lemmas	inl-do-apply, p-fun-exp wf, le wf